ds:x:Id fp Type, da:k:Knd fp Type, l: List, A:ecl-trans-tuple{i:l}(ds;da).
ecl-add-catch(A;l)  ecl-trans-tuple{i:l}(ds;da) 

latex

Definitions	t  T, , P  Q, False, A, AB, , x:A. B(x), S  T, NatDeq, EqDecider(T), list-diff(eq;as;bs), false, , p  q, reduce(f;k;as), i=j, p  q, deq-member(eq;x;L), b, Valtype(da;k), State(ds), Knd, (x  l), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-add-catch(A;l), ecl-trans-tuple{i:l}(ds;da), Id, x. t(x), a:A fp B(a), filter(P;l)
Lemmas	filter wf, nat plus inc, ecl-trans-tuple wf, fpf wf, Id wf, l member wf, Knd wf, decl-state wf, ma-valtype wf, bnot wf, deq-member wf, band wf, eq int wf, reduce wf, bor wf, bool wf, bfalse wf, nat wf, list-diff wf, nat plus wf, nat-deq wf